$\vdash$  $\forall$$T$:Type, $x$, $y$, $z$:$T$. ($\neg$($y$ = $z$)) $\Rightarrow$ ((($x$ = $y$) $\Rightarrow$ ($x$ = $z$)) $\Leftarrow\!\Rightarrow$ ($\neg$($x$ = $y$)))